f:(). (n:. ((f(n))))  (mu(f)  ) 

latex

Definitions	t  T, sq_type(T), x:A. B(x), P  Q, guard(T), prop{i:l}, , x:A. B(x), P  Q, A  B, A, False, T, True, decidable(P), P  Q
Lemmas	decidable int equal, le wf, assert wf, squash wf, true wf, bool wf, nat properties, nat wf